T:Type, x, y:T, L1, L2:(T List).
adjacent(T;L1 @ L2;x;y)
 (adjacent(T;L1;x;y)
  ((0 < ||L1||) & (0 < ||L2||) & x = last(L1) & y = hd(L2))
  adjacent(T;L2;x;y)) 

latex

ProofTree

Definitions

i  j , ||as||, b, A, Type, type List, a < b, {i..j}, s = t, x:A  B(x), P & Q, x:A. B(x), left + right, P  Q, , {x:A| B(x)} , t  T, x:AB(x), P  Q, x:A. B(x), hd(l), last(L), <a, b>, #$n, , False, Void, A c B, A  B, l[i], , n+m, -n, n - m, i  j < k, P  Q, as @ bs, Dec(P), P  Q, Atom, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, f(a), x f y, |r|, xL. P(x), (xL.P(x)), x:A.B(x), x. t(x), (x  l), adjacent(T;L;x;y), {T}, [car / cdr], True, null(as), T, s ~ t, i <z j, i z j, , Top, S  T, []

Lemmas

select cons hd, length-append, top wf, nat wf, member wf, squash wf, true wf, select append back, non neg length, length append, select append front, le wf, iff wf, decidable or, decidable lt, decidable ex int seg, decidable cand, append wf, rev implies wf, length wf1, select wf, last wf, false wf, hd wf, int seg wf, assert wf, not wf